Nuprl Lemma : fpf-all-empty
0,22
postcript
pdf
A
:Type,
eq
,
P
:Top.
y
dom().
w
=(
y
)
P
(
y
,
w
)
True
latex
Definitions
Top
,
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
x
dom(
f
)
,
b
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
(
s1
,
s2
)
,
False
,
t
T
,
True
Lemmas
true
wf
,
false
wf
,
top
wf
origin